|
|
Next Generation of Rank-Based Algorithms for Omega Automata
Šmahlíková, Barbora ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
Büchi automata (BA) complementation is a crucial operation for termination analysis of programs, model checking, or decision procedures for various logics. Despite its prominence, practically efficient algorithms for BA complementation are still missing. This thesis deals with optimizations of Büchi automata complementation, focusing mainly on rank-based techniques. The original rank-based algorithm is asymptotically optimal, but it can still generate unnecessarily large state space. For a practical usage, it is therefore desirable to reduce the number of generated states in the complement as much as possible. We propose several techniques that can efficiently complement some special types of Büchi automata, occuring often in practice, based on their structure. Some of these techniques can also, to a certain degree, be extended to general Büchi automata. The developed techniques were implemented as an extension of the tool Ranker for Büchi automata complementation and evaluated on thousands of hard automata. Our optimizations significantly reduce the generated state space and Ranker produces in the majority of cases a~smaller complement than other state-of-the-art tools.
|
|
|
Efektivní algoritmy pro práci s Büchiho automaty
Laščák, Tomáš ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
Cílem této práce je rozšířit existující knihovnu VATA o modul pro práci s Büchiho automaty, které se řadí mezi konečně stavové automaty nad nekonečnými slovy. Tyto automaty jsou využívány v různých oblastech informatiky, mimo jiné také ve formální verifikaci, při LTL model checkingu. LTL model checking se provádí typicky za pomocí operace testování jazykové inkluze mezi dvěma Büchiho automaty. Protože jazyková inkluze může být výpočetně velmi náročná, vzniklo několik optimalizovaných algoritmů pro tento problém, jako je například přístup založený na Ramseyho větě. Předkládaná práce je zaměřena na tento přístup, jehož implementace je přidána do nově vytvořeného rozšíření knihovny VATA. Mimo to jsou do tohoto nového rozšíření přidány také další operace nad Büchiho automaty, jako jsou sjednocení, průnik nebo redukce počtu stavů.
|
|
|
A Library for Computing Simulation Relations over Büchi Automata
Odvárka, Daniel ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
This thesis presents the topic of simulation relations over Büchi automata and the use case of various simulations. The simulation relations are important for reducing a state space of an automaton, or checking the under approximation of language inclusion. There are also parity games, which are important for computing some of the simulation types we introduce. We will go over multiple algorithms that compute these simulation relations. The mentioned algorithms are implemented in programming language C++ and are compared to a tool named RABIT. Our implementation is better only for smaller sized automata.
|
|
|
Nástroj pro práci s Büchi automaty
Schindler, Petr ; Lengál, Ondřej (oponent) ; Rogalewicz, Adam (vedoucí práce)
Tato práce zpracovává problematiku Büchiho automatů a představuje knihovnu, umožňující provádět základní operace nad těmito automaty. V práci jsou uvedeny základy teorie automatů. Ty jsou použity při popisu konečných automatů, mezi které patří Büchiho automaty, jejichž popis tvoří hlavní část zde uvedené teorie. Znalost jejich vlastností je důležitá pro pochopení algoritmů, které s nimi pracují. Dále jsou tyto algoritmy představeny i s detailním vysvětlením. Následuje návrh datových struktur formátu, v jakém jsou automaty ukládány na disk. Stěžejní část práce se věnuje implementaci knihovny a pomocných skriptů. Detailně jsou zde popsány důležité nebo zajímavé části implementace jednotlivých metod. Závěr práce je věnován testování funkčnosti knihovny.
|
|
|
Next Generation of Rank-Based Algorithms for Omega Automata
Šmahlíková, Barbora ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
Büchi automata (BA) complementation is a crucial operation for termination analysis of programs, model checking, or decision procedures for various logics. Despite its prominence, practically efficient algorithms for BA complementation are still missing. This thesis deals with optimizations of Büchi automata complementation, focusing mainly on rank-based techniques. The original rank-based algorithm is asymptotically optimal, but it can still generate unnecessarily large state space. For a practical usage, it is therefore desirable to reduce the number of generated states in the complement as much as possible. We propose several techniques that can efficiently complement some special types of Büchi automata, occuring often in practice, based on their structure. Some of these techniques can also, to a certain degree, be extended to general Büchi automata. The developed techniques were implemented as an extension of the tool Ranker for Büchi automata complementation and evaluated on thousands of hard automata. Our optimizations significantly reduce the generated state space and Ranker produces in the majority of cases a~smaller complement than other state-of-the-art tools.
|
|
|
A Library for Computing Simulation Relations over Büchi Automata
Odvárka, Daniel ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
This thesis presents the topic of simulation relations over Büchi automata and the use case of various simulations. The simulation relations are important for reducing a state space of an automaton, or checking the under approximation of language inclusion. There are also parity games, which are important for computing some of the simulation types we introduce. We will go over multiple algorithms that compute these simulation relations. The mentioned algorithms are implemented in programming language C++ and are compared to a tool named RABIT. Our implementation is better only for smaller sized automata.
|
|
|
Efektivní algoritmy pro práci s Büchiho automaty
Laščák, Tomáš ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
Cílem této práce je rozšířit existující knihovnu VATA o modul pro práci s Büchiho automaty, které se řadí mezi konečně stavové automaty nad nekonečnými slovy. Tyto automaty jsou využívány v různých oblastech informatiky, mimo jiné také ve formální verifikaci, při LTL model checkingu. LTL model checking se provádí typicky za pomocí operace testování jazykové inkluze mezi dvěma Büchiho automaty. Protože jazyková inkluze může být výpočetně velmi náročná, vzniklo několik optimalizovaných algoritmů pro tento problém, jako je například přístup založený na Ramseyho větě. Předkládaná práce je zaměřena na tento přístup, jehož implementace je přidána do nově vytvořeného rozšíření knihovny VATA. Mimo to jsou do tohoto nového rozšíření přidány také další operace nad Büchiho automaty, jako jsou sjednocení, průnik nebo redukce počtu stavů.
|
|
|
Nástroj pro práci s Büchi automaty
Schindler, Petr ; Lengál, Ondřej (oponent) ; Rogalewicz, Adam (vedoucí práce)
Tato práce zpracovává problematiku Büchiho automatů a představuje knihovnu, umožňující provádět základní operace nad těmito automaty. V práci jsou uvedeny základy teorie automatů. Ty jsou použity při popisu konečných automatů, mezi které patří Büchiho automaty, jejichž popis tvoří hlavní část zde uvedené teorie. Znalost jejich vlastností je důležitá pro pochopení algoritmů, které s nimi pracují. Dále jsou tyto algoritmy představeny i s detailním vysvětlením. Následuje návrh datových struktur formátu, v jakém jsou automaty ukládány na disk. Stěžejní část práce se věnuje implementaci knihovny a pomocných skriptů. Detailně jsou zde popsány důležité nebo zajímavé části implementace jednotlivých metod. Závěr práce je věnován testování funkčnosti knihovny.
|
host ::
RSS.